| Definitions |  x:A. B(x), P   Q, Valtype(da;k), P  Q, ecl-es-act(es;m;x), ecl-act(ds;da;m;x), Prop, t  T,   x. t(x), P  Q, P & Q, if b t else f fi,  x:A. B(x), P Q, A & B, x,y. t(x;y), true, false,  , A B,  A, False, {T}, e(e1,e2].P(e),  , (x l), S  T,  T, True, e[e1,e2).P(e), xL. P(x), e e' , star-append(T;P;Q), {i..j }, i j < k, SQType(T), as @ bs, concat(ll), map(f;as), upto(n), Y, i=j, reduce(f;k;as), S  T, Top, es-hist{i:l}(es;e1;e2), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), ||as||,  , x(s), x(s1,s2), Unit, (e <loc e'), e[e1,e2].P(e), Trans x,y:T. E(x;y), Dec(P),  b, null(as),  |
| Lemmas | ecl-induction, false wf, es-loc wf, nat wf, es-E wf, es-valtype wf, ma-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, Id wf, id-deq wf, top wf, event system wf, decl-state wf, bool wf, ecl-es-act wf, existse-between3 wf, not wf, assert wf, es-first wf, ecl-es-halt wf, es-pred wf, es-loc-pred, es-hist wf, iff wf, l-all wf, l member wf, alle-between1 wf, iseg wf, es-pstar-q wf, iff transitivity, eqtt to assert, assert of eq int, eqff to assert, assert of bnot, not functionality wrt iff, fpf wf, Knd wf, event-info wf, append wf, ecl-halt wf, le wf, ecl-act wf, ecl-es-halt-ecl-halt, es-locl-iff, es-le-loc, es-hist-partition, es-hist-is-append, ecl-halt-nil, ecl-act-nil, iseg-es-hist, l-all-iff, nat plus wf, ecl-halt-ex, nat plus inc, cons member, ecl-ex wf, length wf1, select wf, es-locl wf, es-le wf, non neg length, es-hist-iseg, es-hist-one-one, es-le-trans, es-locl-antireflexive, map wf, int seg wf, upto wf, member map, nat plus properties, decidable int equal, es-interval wf, eq int wf, bnot wf, map append sq, concat append, append assoc sq, concat wf, squash wf, true wf, append-nil, l all wf, decidable assert, null wf3, decidable es-le, decidable es-locl, es-le-not-locl, null-es-hist, assert of null, es-hist-is-concat, Id sq, select member, bool cases, bool sq |
Type, da:k:Knd fp
ds(x)?Top)
